Эту лекцию читал "Грушо Александр Александрович".

1982 год - первая статья о "модели невлияния"

основная идея:
    Добиться: в том, что я вижу - нет следов того, что от меня скрывают.

    фраза абстрактна и не совсем ясно, как её понимать:
        "вижу"
            где?
            язык?
            память? (есть ли память в том, что я вижу)
        "следов"
            что это значит?
            язык? (как выражается след?)
            как увидеть? (этот след)
        "от меня скрывают"
            где? скрывают
            что? можно скрыть
            язык? того, что скрывают
            время? того, что скрывают
            средство анализа?

    видеть можно глазами кусочек чего-то, а можно видеть всю иерархию
    след может представлять из себя как некоторую запись, слов или если мы смотрим на большой язык, то следы ищутся на всех уровнях большой реализации
    важно понимать, где скрывают, и надо понимать, что скрывают - могут скрывать много данных, неизвестный бессмысленный сигнал или одну маленькую команду.
    Если знаешь язык, на котором скрывают, то гораздо проще разобраться. По времени - вчера не скрывали, сегодня скрывают, а завтра я могу предсказать где и что сокроют.


MLS - Multi Level Security - Многоуровневая модель.
    В самом просто случае есть 2 уровня - Высокий и низкий.
    Можно читать вниз, и писать вверх.
    Процесс, который используется для чтения информации на низком уровне, должен найти информацию, которая интересует верхний уровень, прочесть и отправить наверх. Однако тут есть слово "найти", и нижний уровень видит, что ищет верхний уровень - и это нарушение модели Белла-ЛаПадулы.

    Реальный пример:
        Есть сайт гос. закупок, следственный комитет возьмёт именно оттуда информацию организации гос. закупок. Это приведёт к тому, что ясно, что следственый комитет ищет и следовательно у соответствующей компании могут упасть акции (мало ли что там следственный комитет накопает)

    Есть 3 подхода решения проблемы:
        1) передача с низкого уровня на высокий всё, что есть, а уже там разбираться, однако это технически и экономически непримемлимо.
        2) чтение необходимой информации и чтение ещё x записей - однако это строго не доказуемо математически (вегда остаётся вероятность угодать)
            Он со мной не согласился: однако в целом, первый случай - это частный крайний случай этого предложенного, и всегда есть вероятность угодать, какая информация была нужна, т.е. осталось лишь просто сойтись в приемлимой вероятности угадывания.
        3) пытаться анонимизировать чтение, кем бы оно ни поводилось, однако есть проблема

CSP - Communicating sequential processes - язык для записи процессов.
    c!v - P
    c?v - P(v)

    copy = in ? v -> out ! x -> copy

    traces (copy) = {<>}  и  {in v, v принадлежит V}  и  {<in v, out v>, v принадлежит V}

High    S   H
Low     S   L
High не включает Low через S <=> 
    для любого trace, output L S(tr, c) (n/t/ если берётся trace системы и передаётся по каналу с), =
        = то совпадает с = output L S(trace без L, c)
    Т.е. по сути это и есть запись, что то, что мы видим не даёт следов о том, что мы пытаемся скрыть.

допустимые trace:
    {<>, <l>, <l, h>, <lh, l2>}
    S = l -> h -> l2 -> stop -> ll2
        Это самая большая слабость модели невлияния.

Модель невлияния должна гарантировать, что ничего лишнего сверху не будет видно

Класс математических теорем, которые доказываются в той или иной модели, и состоящие в том, что 
    Если мы хотим доказать теорию невлияния, то её теоретически нужно доказать для бесконечного количества слов, хотя сами пользуемся вполне конкретными схемами.
    Поэтому доказывается сначало для простого trace, а потом переносится на общие случаи, например, по индукции.

Автоматные модели невлияния.
    Автомат = {входной алфавит, множество состояний, выходной алфавит, отображение входного алфавита * состояние -> состояние, отображение входного алфавита * состояние -> выходное состояние}

    последнее отображение мы выкинем, и будем преимущественно пользовать именно отображение в состояния.

    Состояние = множество состояний low * множество состояний high = {(s-low, s-high)}

    В автоматных моделях есть классическая и модель, рассмотренная в анализе реальных систем, при построении модели безопасности.
    X = X-high * X-Low

    Функция перехода (это самое важное):
        Если x принадлежит S-high (x, (s-high, s-low)) -> (s-high', s-low)
        Если x принадлежит S-low (x, (s-high, s-low)) -> (s-high, s-low')
        "->" === ("-low->", "-high->")

    Введём отношение эквивалентности: S -=- S' <=> s-low = S-low'
    Множество классов эквивалентности изоморфно S-low
    Тогда отображение "-low->" определяется как X-low * S-low = S-low

    Теорема 1.
        Справедлива следующая коммутативная диаграмма

               ->          S             ->
        X*S                                        S-low
               ->    X-low * S-low     -low->

    Дальше вроде бы по индукции это распространяется на большие слова

Модель плоха тем, что есть канал, который позволяет получить информацию о high


Допустим есть автомат High и автомат Low.
Гомоморфизм автоматов означает, что есть отображение, которое сюрьективно (т.е. некоторые слова алфавита, или некоторые состояния одного автомата исправно с учётом отображеия отржаются на другой автомат, но некоторые могут стать идентичными)
Между исходным автоматом и автоматом Low присутствует гомоморфизм (следует из диаграммы теоремы 1)

Если мы рассмотрим автомат
с 2-мя входами Low и 2-мя входами High и соответственно такими же 4-я выходами, то благодаря гомоморфизму, мы в нём можем замнукть low на low и high на high и автомат всё равно будет удовлетворять модели невлияния.
Если автомат зациклен на искось, то мы получаем фактически сеть.

Эта модель взялась, когда выяснилось, что вставлять заплатку в каждый процессор - то она становится невидимой и очень дешёвой, а если вставлять в один проц, то это видно и дорого.


Книжечки:
    Милман - Concurrency Processes
    Райн и Шнейр - Многопроцессная алгебра и невлияние. (CSFW 12)